We introduce a generic extension of the popular branching-time logic CTLwhich refines the temporal until and release operators with formal languages.For instance, a language may determine the moments along a path that an untilproperty may be fulfilled. We consider several classes of languages leading tologics with different expressive power and complexity, whose importance ismotivated by their use in model checking, synthesis, abstract interpretation,etc. We show that even with context-free languages on the until operator the logicstill allows for polynomial time model-checking despite the significantincrease in expressive power. This makes the logic a promising candidate forapplications in verification. In addition, we analyse the complexity of satisfiability and compare theexpressive power of these logics to CTL* and extensions of PDL.
展开▼
